Inhalt des Dokuments
Publikationen
| Zitatschlüssel | bisping2016constructive |
|---|---|
| Autor | Bisping, Benjamin and Brodmann, Paul-David and Jungnickel, Tim and Rickmann, Christina and Seidler, Henning and Stüber, Anke and Wilhelm-Weidner, Arno and Peters, Kirstin and Nestmann, Uwe |
| Jahr | 2016 |
| Journal | Archive of Formal Proofs |
| Jahrgang | 2016 |
| Notiz | http://isa-afp.org/entries/FLP.shtml, Formal proof development as described in the conference paper, Mechanical Verification of a Constructive Proof for FLP |
| Zusammenfassung | The impossibility of distributed consensus with one faulty process is a result with important consequences for real world distributed systems e.g., commits in repli- cated databases. Since proofs are not immune to faults and even plausible proofs with a profound formalism can conclude wrong results, we validate the fundamen- tal result named FLP after Fischer, Lynch and Paterson by using the interactive theorem prover Isabelle/HOL. We present a formalization of distributed systems and the aforementioned consensus problem. Our proof is based on Hagen V ̈olzer’s paper A constructive proof for FLP. In addition to the enhanced confidence in the validity of V ̈olzer’s proof, we contribute the missing gaps to show the correctness in Isabelle/HOL. We clarify the proof details and even prove fairness of the infinite execution that contradicts consensus. Our Isabelle formalization can also be reused for further proofs of properties of distributed systems. |
Zusatzinformationen / Extras
Direktzugang
Schnellnavigation zur Seite über Nummerneingabe